rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
↳ QTRS
↳ DependencyPairsProof
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
REV2(x, ++(y, z)) → REV(++(x, rev(rev2(y, z))))
REV(++(x, y)) → REV1(x, y)
REV1(x, ++(y, z)) → REV1(y, z)
REV2(x, ++(y, z)) → REV2(y, z)
REV2(x, ++(y, z)) → REV(rev2(y, z))
REV(++(x, y)) → REV2(x, y)
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
REV2(x, ++(y, z)) → REV(++(x, rev(rev2(y, z))))
REV(++(x, y)) → REV1(x, y)
REV1(x, ++(y, z)) → REV1(y, z)
REV2(x, ++(y, z)) → REV2(y, z)
REV2(x, ++(y, z)) → REV(rev2(y, z))
REV(++(x, y)) → REV2(x, y)
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
REV1(x, ++(y, z)) → REV1(y, z)
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REV1(x, ++(y, z)) → REV1(y, z)
The value of delta used in the strict ordering is 4.
POL(++(x1, x2)) = 1 + (4)x_2
POL(REV1(x1, x2)) = (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
REV2(x, ++(y, z)) → REV(++(x, rev(rev2(y, z))))
REV2(x, ++(y, z)) → REV2(y, z)
REV2(x, ++(y, z)) → REV(rev2(y, z))
REV(++(x, y)) → REV2(x, y)
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REV2(x, ++(y, z)) → REV(++(x, rev(rev2(y, z))))
REV2(x, ++(y, z)) → REV2(y, z)
REV2(x, ++(y, z)) → REV(rev2(y, z))
REV(++(x, y)) → REV2(x, y)
The value of delta used in the strict ordering is 1/16.
POL(REV2(x1, x2)) = (1/2)x_2
POL(++(x1, x2)) = 1/4 + (4)x_2
POL(rev2(x1, x2)) = x_2
POL(REV(x1)) = (1/4)x_1
POL(rev(x1)) = x_1
POL(nil) = 0
POL(rev1(x1, x2)) = 0
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))